the_es:ES, e':E, l:IdLnk, n:{0..(||sends(l;e')||+1)}, m:Msg.
(m  snds(l, before(e',n)))
 ((e:E. ((e <loc e') & (m  sends(l;e))))  (i:{0..n}. (m = sends(l;e')[i]))) 

latex

Definitions	x:A. B(x), P  Q, snds(l, before(e,n)), P  Q, x:A. B(x), P & Q, P  Q, , P  Q, t  T, S  T, A  B, A, False, {i..j}, (Msg on l), i  j < k
Lemmas	iff functionality wrt iff, l member wf, append wf, es-snds wf, firstn wf, es-sends wf, es-locl wf, int seg wf, select wf, member append, or functionality wrt iff, member-es-snds, member-firstn, es-Msg wf, length wf1, es-Msgl wf, IdLnk wf, es-E wf, event system wf